type name;
type ref;
const unique null : ref;
type real;
type elements;
type struct;
type exposeVersionType;
var $Heap : <x>[ref, name]x where IsHeap($Heap);
function IsHeap(h : <x>[ref, name]x) returns ($$unnamed~a : bool);
const $allocated : name;
const $elements : name;
const $inv : name;
const $localinv : name;
const $exposeVersion : name;
axiom (DeclType($exposeVersion) == System.Object);
const $sharingMode : name;
const $SharingMode_Unshared : name;
const $SharingMode_LockProtected : name;
const $ownerRef : name;
const $ownerFrame : name;
const $PeerGroupPlaceholder : name;
function ClassRepr(class : name) returns ($$unnamed~b : ref);
axiom (forall c0 : name, c1 : name :: {ClassRepr(c0), ClassRepr(c1)} ((c0 != c1) ==> (ClassRepr(c0) != ClassRepr(c1))));
axiom (forall T : name :: !($typeof(ClassRepr(T)) <: System.Object));
axiom (forall T : name :: (ClassRepr(T) != null));
axiom (forall T : name, h : <x>[ref, name]x :: {h[ClassRepr(T), $ownerFrame]} (IsHeap(h) ==> (h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder)));
function IsDirectlyModifiableField(f : name) returns ($$unnamed~c : bool);
axiom !IsDirectlyModifiableField($allocated);
axiom IsDirectlyModifiableField($elements);
axiom !IsDirectlyModifiableField($inv);
axiom !IsDirectlyModifiableField($localinv);
axiom !IsDirectlyModifiableField($ownerRef);
axiom !IsDirectlyModifiableField($ownerFrame);
axiom !IsDirectlyModifiableField($exposeVersion);
function IsStaticField(f : name) returns ($$unnamed~d : bool);
axiom !IsStaticField($allocated);
axiom !IsStaticField($elements);
axiom !IsStaticField($inv);
axiom !IsStaticField($localinv);
axiom !IsStaticField($exposeVersion);
function ValueArrayGet<any>($$unnamed~f : elements, $$unnamed~e : int) returns ($$unnamed~g : any);
function ValueArraySet<any>($$unnamed~j : elements, $$unnamed~i : int, $$unnamed~h : any) returns ($$unnamed~k : elements);
function RefArrayGet($$unnamed~m : elements, $$unnamed~l : int) returns ($$unnamed~n : ref);
function RefArraySet($$unnamed~q : elements, $$unnamed~p : int, $$unnamed~o : ref) returns ($$unnamed~r : elements);
axiom (forall<any> A : elements, i : int, x : any :: (ValueArrayGet(ValueArraySet(A, i, x), i) == x));
axiom (forall<any> A : elements, i : int, j : int, x : any :: ((i != j) ==> (ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j))));
axiom (forall A : elements, i : int, x : ref :: (RefArrayGet(RefArraySet(A, i, x), i) == x));
axiom (forall A : elements, i : int, j : int, x : ref :: ((i != j) ==> (RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j))));
function ArrayIndex(arr : ref, dim : int, indexAtDim : int, remainingIndexContribution : int) returns ($$unnamed~s : int);
axiom (forall a : ref, d : int, x : int, y : int, x' : int, y' : int :: {ArrayIndex(a, d, x, y), ArrayIndex(a, d, x', y')} ((ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y')) ==> ((x == x') && (y == y'))));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: RefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: RefArray(T, r))) ==> $Is(RefArrayGet(heap[a, $elements], i), T)));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: NonNullRefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: NonNullRefArray(T, r))) ==> $IsNotNull(RefArrayGet(heap[a, $elements], i), T)));
function $Rank($$unnamed~t : ref) returns ($$unnamed~u : int);
axiom (forall a : ref :: (1 <= $Rank(a)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: RefArray(T, r))} (((a != null) && ($typeof(a) <: RefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: NonNullRefArray(T, r))} (((a != null) && ($typeof(a) <: NonNullRefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: ValueArray(T, r))} (((a != null) && ($typeof(a) <: ValueArray(T, r))) ==> ($Rank(a) == r)));
function $Length($$unnamed~v : ref) returns ($$unnamed~w : int);
axiom (forall a : ref :: {$Length(a)} (0 <= $Length(a)));
function $DimLength($$unnamed~y : ref, $$unnamed~x : int) returns ($$unnamed~z : int);
axiom (forall a : ref, i : int :: (0 <= $DimLength(a, i)));
axiom (forall a : ref :: {$DimLength(a, 0)} (($Rank(a) == 1) ==> ($DimLength(a, 0) == $Length(a))));
function $LBound($$unnamed~ab : ref, $$unnamed~aa : int) returns ($$unnamed~ac : int);
function $UBound($$unnamed~ae : ref, $$unnamed~ad : int) returns ($$unnamed~af : int);
axiom (forall a : ref, i : int :: {$LBound(a, i)} ($LBound(a, i) == 0));
axiom (forall a : ref, i : int :: {$UBound(a, i)} ($UBound(a, i) == ($DimLength(a, i) - 1)));
const $ArrayCategoryValue : name;
const $ArrayCategoryRef : name;
const $ArrayCategoryNonNullRef : name;
function $ArrayCategory(arrayType : name) returns (arrayCategory : name);
axiom (forall T : name, ET : name, r : int :: {(T <: ValueArray(ET, r))} ((T <: ValueArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryValue)));
axiom (forall T : name, ET : name, r : int :: {(T <: RefArray(ET, r))} ((T <: RefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryRef)));
axiom (forall T : name, ET : name, r : int :: {(T <: NonNullRefArray(ET, r))} ((T <: NonNullRefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryNonNullRef)));
const System.Array : name;
axiom (System.Array <: System.Object);
function $ElementType($$unnamed~ag : name) returns ($$unnamed~ah : name);
function ValueArray(elementType : name, rank : int) returns ($$unnamed~ai : name);
axiom (forall T : name, r : int :: {ValueArray(T, r)} (ValueArray(T, r) <: System.Array));
function RefArray(elementType : name, rank : int) returns ($$unnamed~aj : name);
axiom (forall T : name, r : int :: {RefArray(T, r)} (RefArray(T, r) <: System.Array));
function NonNullRefArray(elementType : name, rank : int) returns ($$unnamed~ak : name);
axiom (forall T : name, r : int :: {NonNullRefArray(T, r)} (NonNullRefArray(T, r) <: System.Array));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (RefArray(U, r) <: RefArray(T, r))));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (NonNullRefArray(U, r) <: NonNullRefArray(T, r))));
axiom (forall A : name, r : int :: ($ElementType(ValueArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(RefArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(NonNullRefArray(A, r)) == A));
axiom (forall A : name, r : int, T : name :: {(T <: RefArray(A, r))} ((T <: RefArray(A, r)) ==> ((T == RefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: NonNullRefArray(A, r))} ((T <: NonNullRefArray(A, r)) ==> ((T == NonNullRefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: ValueArray(A, r))} ((T <: ValueArray(A, r)) ==> (T == ValueArray(A, r))));
axiom (forall A : name, r : int, T : name :: ((RefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == RefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((NonNullRefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == NonNullRefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((ValueArray(A, r) <: T) ==> ((System.Array <: T) || (T == ValueArray(A, r)))));
function $ArrayPtr(elementType : name) returns ($$unnamed~al : name);
function $StructGet<any>($$unnamed~an : struct, $$unnamed~am : name) returns ($$unnamed~ao : any);
function $StructSet<any>($$unnamed~ar : struct, $$unnamed~aq : name, $$unnamed~ap : any) returns ($$unnamed~as : struct);
axiom (forall<any> s : struct, f : name, x : any :: ($StructGet($StructSet(s, f, x), f) == x));
axiom (forall<any> s : struct, f : name, f' : name, x : any :: ((f != f') ==> ($StructGet($StructSet(s, f, x), f') == $StructGet(s, f'))));
function ZeroInit(s : struct, typ : name) returns ($$unnamed~at : bool);
function $typeof($$unnamed~au : ref) returns ($$unnamed~av : name);
function $BaseClass(sub : name) returns (base : name);
function AsDirectSubClass(sub : name, base : name) returns (sub' : name);
function OneClassDown(sub : name, base : name) returns (directSub : name);
axiom (forall A : name, B : name, C : name :: {(C <: AsDirectSubClass(B, A))} ((C <: AsDirectSubClass(B, A)) ==> (OneClassDown(C, A) == B)));
function $IsValueType($$unnamed~aw : name) returns ($$unnamed~ax : bool);
axiom (forall T : name :: ($IsValueType(T) ==> ((forall U : name :: ((T <: U) ==> (T == U))) && (forall U : name :: ((U <: T) ==> (T == U))))));
const System.Object : name;
function $IsTokenForType($$unnamed~az : struct, $$unnamed~ay : name) returns ($$unnamed~ba : bool);
function TypeObject($$unnamed~bb : name) returns ($$unnamed~bc : ref);
const System.Type : name;
axiom (System.Type <: System.Object);
axiom (forall T : name :: {TypeObject(T)} $IsNotNull(TypeObject(T), System.Type));
function TypeName($$unnamed~bd : ref) returns ($$unnamed~be : name);
axiom (forall T : name :: {TypeObject(T)} (TypeName(TypeObject(T)) == T));
function $Is($$unnamed~bg : ref, $$unnamed~bf : name) returns ($$unnamed~bh : bool);
axiom (forall o : ref, T : name :: {$Is(o, T)} ($Is(o, T) <==> ((o == null) || ($typeof(o) <: T))));
function $IsNotNull($$unnamed~bj : ref, $$unnamed~bi : name) returns ($$unnamed~bk : bool);
axiom (forall o : ref, T : name :: {$IsNotNull(o, T)} ($IsNotNull(o, T) <==> ((o != null) && $Is(o, T))));
function $As($$unnamed~bm : ref, $$unnamed~bl : name) returns ($$unnamed~bn : ref);
axiom (forall o : ref, T : name :: ($Is(o, T) ==> ($As(o, T) == o)));
axiom (forall o : ref, T : name :: (!$Is(o, T) ==> ($As(o, T) == null)));
axiom (forall h : <x>[ref, name]x, o : ref :: {($typeof(o) <: System.Array), h[o, $inv]} (((IsHeap(h) && (o != null)) && ($typeof(o) <: System.Array)) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
function IsAllocated<any>(h : <x>[ref, name]x, o : any) returns ($$unnamed~bo : bool);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {IsAllocated(h, h[o, f])} ((IsHeap(h) && h[o, $allocated]) ==> IsAllocated(h, h[o, f])));
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[h[o, f], $allocated]} ((IsHeap(h) && h[o, $allocated]) ==> h[h[o, f], $allocated]));
axiom (forall h : <x>[ref, name]x, s : struct, f : name :: {IsAllocated(h, $StructGet(s, f))} (IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, RefArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, ValueArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, o : ref :: {h[o, $allocated]} (IsAllocated(h, o) ==> h[o, $allocated]));
axiom (forall h : <x>[ref, name]x, c : name :: {h[ClassRepr(c), $allocated]} (IsHeap(h) ==> h[ClassRepr(c), $allocated]));
const $BeingConstructed : ref;
const $NonNullFieldsAreInitialized : name;
function DeclType(field : name) returns (class : name);
function AsNonNullRefField(field : name, T : name) returns (f : name);
function AsRefField(field : name, T : name) returns (f : name);
function AsRangeField(field : name, T : name) returns (f : name);
axiom (forall f : name, T : name :: {AsNonNullRefField(f, T)} ((AsNonNullRefField(f, T) == f) ==> (AsRefField(f, T) == f)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRefField(f, T)]} (IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsNonNullRefField(f, T)]} (((IsHeap(h) && (o != null)) && ((o != $BeingConstructed) || (h[$BeingConstructed, $NonNullFieldsAreInitialized] == true))) ==> (h[o, AsNonNullRefField(f, T)] != null)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRangeField(f, T)]} (IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)));
function $IsMemberlessType($$unnamed~bp : name) returns ($$unnamed~bq : bool);
axiom (forall o : ref :: {$IsMemberlessType($typeof(o))} !$IsMemberlessType($typeof(o)));
function $IsImmutable(T : name) returns ($$unnamed~br : bool);
axiom !$IsImmutable(System.Object);
function $AsImmutable(T : name) returns (theType : name);
function $AsMutable(T : name) returns (theType : name);
axiom (forall T : name, U : name :: {(U <: $AsImmutable(T))} ((U <: $AsImmutable(T)) ==> ($IsImmutable(U) && ($AsImmutable(U) == U))));
axiom (forall T : name, U : name :: {(U <: $AsMutable(T))} ((U <: $AsMutable(T)) ==> (!$IsImmutable(U) && ($AsMutable(U) == U))));
function AsOwner(string : ref, owner : ref) returns (theString : ref);
axiom (forall o : ref, T : name :: {($typeof(o) <: $AsImmutable(T))} ((((o != null) && (o != $BeingConstructed)) && ($typeof(o) <: $AsImmutable(T))) ==> (forall h : <x>[ref, name]x :: {IsHeap(h)} (IsHeap(h) ==> (((((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o))) && (h[o, $ownerFrame] == $PeerGroupPlaceholder)) && (AsOwner(o, h[o, $ownerRef]) == o)) && (forall t : ref :: {AsOwner(o, h[t, $ownerRef])} ((AsOwner(o, h[t, $ownerRef]) == o) ==> ((t == o) || (h[t, $ownerFrame] != $PeerGroupPlaceholder)))))))));
const System.String : name;
function $StringLength($$unnamed~bs : ref) returns ($$unnamed~bt : int);
axiom (forall s : ref :: {$StringLength(s)} (0 <= $StringLength(s)));
function AsRepField(f : name, declaringType : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRepField(f, T)]} ((IsHeap(h) && (h[o, AsRepField(f, T)] != null)) ==> ((h[h[o, AsRepField(f, T)], $ownerRef] == o) && (h[h[o, AsRepField(f, T)], $ownerFrame] == T))));
function AsPeerField(f : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[o, AsPeerField(f)]} ((IsHeap(h) && (h[o, AsPeerField(f)] != null)) ==> ((h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef]) && (h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]))));
axiom (forall h : <x>[ref, name]x, o : ref :: {(h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])} ((((IsHeap(h) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
procedure $SetOwner(o : ref, ow : ref, fr : name);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[o, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[o, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == ow) && ($Heap[p, $ownerFrame] == fr))));
  

procedure $UpdateOwnersForRep(o : ref, T : name, e : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[e, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((e == null) ==> ($Heap == old($Heap)));
  ensures ((e != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[e, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == o) && ($Heap[p, $ownerFrame] == T)))));
  

procedure $UpdateOwnersForPeer(c : ref, d : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} ((((F != $ownerRef) && (F != $ownerFrame)) || old(((($Heap[p, $ownerRef] != $Heap[c, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[c, $ownerFrame])) && (($Heap[p, $ownerRef] != $Heap[d, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]))))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((d == null) ==> ($Heap == old($Heap)));
  ensures ((d != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} (((old(($Heap[p, $ownerRef] == $Heap[c, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[c, $ownerFrame]))) || (old(($Heap[p, $ownerRef] == $Heap[d, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[d, $ownerFrame])))) ==> ((((old($Heap)[d, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[c, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame])) || (((old($Heap)[d, $ownerFrame] != $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[d, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[d, $ownerFrame]))))));
  

const $FirstConsistentOwner : name;
function $AsPureObject($$unnamed~bu : ref) returns ($$unnamed~bv : ref);
function ##FieldDependsOnFCO<any>(o : ref, f : name, ev : exposeVersionType) returns (value : any);
axiom (forall o : ref, f : name, h : <x>[ref, name]x :: {h[$AsPureObject(o), f]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion]))));
axiom (forall o : ref, h : <x>[ref, name]x :: {h[o, $FirstConsistentOwner]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (((h[o, $FirstConsistentOwner] != null) && (h[h[o, $FirstConsistentOwner], $allocated] == true)) && (((h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder) || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame])) || (h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))))));
function Box<any>($$unnamed~bx : any, $$unnamed~bw : ref) returns ($$unnamed~by : ref);
function Unbox<any>($$unnamed~bz : ref) returns ($$unnamed~ca : any);
axiom (forall<any> x : any, p : ref :: {Unbox(Box(x, p))} (Unbox(Box(x, p)) == x));
function UnboxedType($$unnamed~cb : ref) returns ($$unnamed~cc : name);
axiom (forall p : ref :: {$IsValueType(UnboxedType(p))} ($IsValueType(UnboxedType(p)) ==> (forall<any> heap : <x>[ref, name]x, x : any :: {heap[Box(x, p), $inv]} (IsHeap(heap) ==> ((heap[Box(x, p), $inv] == $typeof(Box(x, p))) && (heap[Box(x, p), $localinv] == $typeof(Box(x, p))))))));
axiom (forall<any> x : any, p : ref :: {(UnboxedType(Box(x, p)) <: System.Object)} (((UnboxedType(Box(x, p)) <: System.Object) && (Box(x, p) == p)) ==> (x == p)));
function BoxTester(p : ref, typ : name) returns ($$unnamed~cd : ref);
axiom (forall p : ref, typ : name :: {BoxTester(p, typ)} ((UnboxedType(p) == typ) <==> (BoxTester(p, typ) != null)));
const System.SByte : name;
axiom $IsValueType(System.SByte);
const System.Byte : name;
axiom $IsValueType(System.Byte);
const System.Int16 : name;
axiom $IsValueType(System.Int16);
const System.UInt16 : name;
axiom $IsValueType(System.UInt16);
const System.Int32 : name;
axiom $IsValueType(System.Int32);
const System.UInt32 : name;
axiom $IsValueType(System.UInt32);
const System.Int64 : name;
axiom $IsValueType(System.Int64);
const System.UInt64 : name;
axiom $IsValueType(System.UInt64);
const System.Char : name;
axiom $IsValueType(System.Char);
const int#m2147483648 : int;
const int#2147483647 : int;
const int#4294967295 : int;
const int#m9223372036854775808 : int;
const int#9223372036854775807 : int;
const int#18446744073709551615 : int;
axiom (int#m9223372036854775808 < int#m2147483648);
axiom (int#m2147483648 < (0 - 100000));
axiom (100000 < int#2147483647);
axiom (int#2147483647 < int#4294967295);
axiom (int#4294967295 < int#9223372036854775807);
axiom (int#9223372036854775807 < int#18446744073709551615);
function InRange(i : int, T : name) returns ($$unnamed~ce : bool);
axiom (forall i : int :: (InRange(i, System.SByte) <==> (((0 - 128) <= i) && (i < 128))));
axiom (forall i : int :: (InRange(i, System.Byte) <==> ((0 <= i) && (i < 256))));
axiom (forall i : int :: (InRange(i, System.Int16) <==> (((0 - 32768) <= i) && (i < 32768))));
axiom (forall i : int :: (InRange(i, System.UInt16) <==> ((0 <= i) && (i < 65536))));
axiom (forall i : int :: (InRange(i, System.Int32) <==> ((int#m2147483648 <= i) && (i <= int#2147483647))));
axiom (forall i : int :: (InRange(i, System.UInt32) <==> ((0 <= i) && (i <= int#4294967295))));
axiom (forall i : int :: (InRange(i, System.Int64) <==> ((int#m9223372036854775808 <= i) && (i <= int#9223372036854775807))));
axiom (forall i : int :: (InRange(i, System.UInt64) <==> ((0 <= i) && (i <= int#18446744073709551615))));
axiom (forall i : int :: (InRange(i, System.Char) <==> ((0 <= i) && (i < 65536))));
function $IntToInt(val : int, fromType : name, toType : name) returns ($$unnamed~cf : int);
function $IntToReal($$unnamed~cg : int, fromType : name, toType : name) returns ($$unnamed~ch : real);
function $RealToInt($$unnamed~ci : real, fromType : name, toType : name) returns ($$unnamed~cj : int);
function $RealToReal(val : real, fromType : name, toType : name) returns ($$unnamed~ck : real);
function $SizeIs($$unnamed~cm : name, $$unnamed~cl : int) returns ($$unnamed~cn : bool);
function $IfThenElse<any>($$unnamed~cq : bool, $$unnamed~cp : any, $$unnamed~co : any) returns ($$unnamed~cr : any);
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (b ==> ($IfThenElse(b, x, y) == x)));
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (!b ==> ($IfThenElse(b, x, y) == y)));
function #neg($$unnamed~cs : int) returns ($$unnamed~ct : int);
function #and($$unnamed~cv : int, $$unnamed~cu : int) returns ($$unnamed~cw : int);
function #or($$unnamed~cy : int, $$unnamed~cx : int) returns ($$unnamed~cz : int);
function #xor($$unnamed~db : int, $$unnamed~da : int) returns ($$unnamed~dc : int);
function #shl($$unnamed~de : int, $$unnamed~dd : int) returns ($$unnamed~df : int);
function #shr($$unnamed~dh : int, $$unnamed~dg : int) returns ($$unnamed~di : int);
function #rneg($$unnamed~dj : real) returns ($$unnamed~dk : real);
function #radd($$unnamed~dm : real, $$unnamed~dl : real) returns ($$unnamed~dn : real);
function #rsub($$unnamed~dp : real, $$unnamed~do : real) returns ($$unnamed~dq : real);
function #rmul($$unnamed~ds : real, $$unnamed~dr : real) returns ($$unnamed~dt : real);
function #rdiv($$unnamed~dv : real, $$unnamed~du : real) returns ($$unnamed~dw : real);
function #rmod($$unnamed~dy : real, $$unnamed~dx : real) returns ($$unnamed~dz : real);
function #rLess($$unnamed~eb : real, $$unnamed~ea : real) returns ($$unnamed~ec : bool);
function #rAtmost($$unnamed~ee : real, $$unnamed~ed : real) returns ($$unnamed~ef : bool);
function #rEq($$unnamed~eh : real, $$unnamed~eg : real) returns ($$unnamed~ei : bool);
function #rNeq($$unnamed~ek : real, $$unnamed~ej : real) returns ($$unnamed~el : bool);
function #rAtleast($$unnamed~en : real, $$unnamed~em : real) returns ($$unnamed~eo : bool);
function #rGreater($$unnamed~eq : real, $$unnamed~ep : real) returns ($$unnamed~er : bool);
axiom (forall x : int, y : int :: {(x % y)} {(x / y)} ((x % y) == (x - ((x / y) * y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (0 < y)) ==> ((0 <= (x % y)) && ((x % y) < y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (y < 0)) ==> ((0 <= (x % y)) && ((x % y) < (0 - y)))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (0 < y)) ==> (((0 - y) < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (y < 0)) ==> ((y < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {((x + y) % y)} (((0 <= x) && (0 <= y)) ==> (((x + y) % y) == (x % y))));
axiom (forall x : int, y : int :: {((y + x) % y)} (((0 <= x) && (0 <= y)) ==> (((y + x) % y) == (x % y))));
axiom (forall x : int, y : int :: {((x - y) % y)} (((0 <= (x - y)) && (0 <= y)) ==> (((x - y) % y) == (x % y))));
axiom (forall a : int, b : int, d : int :: {(a % d), (b % d)} ((((2 <= d) && ((a % d) == (b % d))) && (a < b)) ==> ((a + d) <= b)));
axiom (forall x : int, y : int :: {#and(x, y)} (((0 <= x) || (0 <= y)) ==> (0 <= #and(x, y))));
axiom (forall x : int, y : int :: {#or(x, y)} (((0 <= x) && (0 <= y)) ==> ((0 <= #or(x, y)) && (#or(x, y) <= (x + y)))));
axiom (forall i : int :: {#shl(i, 0)} (#shl(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shl(i, (j + 1)) == (#shl(i, j) * 2))));
axiom (forall i : int :: {#shr(i, 0)} (#shr(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shr(i, (j + 1)) == (#shr(i, j) / 2))));
function #System.String.IsInterned$System.String$notnull($$unnamed~es : ref) returns ($$unnamed~et : ref);
function #System.String.Equals$System.String($$unnamed~ev : ref, $$unnamed~eu : ref) returns ($$unnamed~ew : bool);
function #System.String.Equals$System.String$System.String($$unnamed~ey : ref, $$unnamed~ex : ref) returns ($$unnamed~ez : bool);
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String(a, b)} (#System.String.Equals$System.String(a, b) == #System.String.Equals$System.String$System.String(a, b)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} (#System.String.Equals$System.String$System.String(a, b) == #System.String.Equals$System.String$System.String(b, a)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} ((((a != null) && (b != null)) && #System.String.Equals$System.String$System.String(a, b)) ==> (#System.String.IsInterned$System.String$notnull(a) == #System.String.IsInterned$System.String$notnull(b))));
const $UnknownRef : ref;
const Thing.f : name;
const Friend.th : name;
const Thing.y : name;
const Friend.x : name;
const System.Reflection.IReflect : name;
const Microsoft.Contracts.ObjectInvariantException : name;
const Thing : name;
const System.Reflection.ICustomAttributeProvider : name;
const System.Runtime.InteropServices._Exception : name;
const System.Runtime.Serialization.ISerializable : name;
const Microsoft.Contracts.GuardException : name;
const Microsoft.Contracts.ICheckedException : name;
const System.Exception : name;
const System.Runtime.InteropServices._MemberInfo : name;
const System.Boolean : name;
const System.Runtime.InteropServices._Type : name;
const Friend : name;
const System.Reflection.MemberInfo : name;
axiom !IsStaticField(Friend.th);
axiom IsDirectlyModifiableField(Friend.th);
axiom (DeclType(Friend.th) == Friend);
axiom (AsRefField(Friend.th, Thing) == Friend.th);
axiom !IsStaticField(Thing.f);
axiom IsDirectlyModifiableField(Thing.f);
axiom (AsPeerField(Thing.f) == Thing.f);
axiom (DeclType(Thing.f) == Thing);
axiom (AsRefField(Thing.f, Friend) == Thing.f);
axiom !IsStaticField(Thing.y);
axiom IsDirectlyModifiableField(Thing.y);
axiom (DeclType(Thing.y) == Thing);
axiom (AsRangeField(Thing.y, System.Int32) == Thing.y);
axiom !IsStaticField(Friend.x);
axiom IsDirectlyModifiableField(Friend.x);
axiom (DeclType(Friend.x) == Friend);
axiom (AsRangeField(Friend.x, System.Int32) == Friend.x);
axiom (Friend <: Friend);
axiom ($BaseClass(Friend) == System.Object);
axiom ((Friend <: $BaseClass(Friend)) && (AsDirectSubClass(Friend, $BaseClass(Friend)) == Friend));
axiom (!$IsImmutable(Friend) && ($AsMutable(Friend) == Friend));
axiom (forall $U : name :: {($U <: Friend)} (($U <: Friend) ==> ($U == Friend)));
axiom (Thing <: Thing);
axiom ($BaseClass(Thing) == System.Object);
axiom ((Thing <: $BaseClass(Thing)) && (AsDirectSubClass(Thing, $BaseClass(Thing)) == Thing));
axiom (!$IsImmutable(Thing) && ($AsMutable(Thing) == Thing));
axiom (forall $U : name :: {($U <: Thing)} (($U <: Thing) ==> ($U == Thing)));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: Thing)} (((IsHeap($h) && ($h[$oi, $inv] <: Thing)) && ($h[$oi, $localinv] != System.Object)) ==> ((($h[$oi, Thing.f] == null) || ($h[$h[$oi, Thing.f], Friend.th] == $oi)) && (0 <= $h[$oi, Thing.y]))));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: Friend)} (((IsHeap($h) && ($h[$oi, $inv] <: Friend)) && ($h[$oi, $localinv] != System.Object)) ==> ((($h[$oi, Friend.th] != null) && ($h[$oi, Friend.x] == $h[$h[$oi, Friend.th], Thing.y])) && ($h[$h[$oi, Friend.th], Thing.f] == $oi))));
axiom (forall $U : name :: {($U <: System.Boolean)} (($U <: System.Boolean) ==> ($U == System.Boolean)));
procedure Friend.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Friend.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  var stack0i : int;
  var stack1i : int;
  var stack50000o : ref;
  var local0 : bool where true;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, Friend); goto $$entry~b;
  $$entry~b: assume ($Heap[this, $allocated] == true); goto $$entry~a;
  $$entry~a: throwException := throwException$in; goto block1751;
  block1751: goto block1768;
  block1768: assert (this != null); goto $$block1768~b;
  $$block1768~b: stack0o := $Heap[this, Friend.th]; goto $$block1768~a;
  $$block1768~a: stack1o := null; goto true1768to1870, false1768to1785;
  true1768to1870: assume (stack0o != stack1o); goto block1870;
  false1768to1785: assume (stack0o == stack1o); goto block1785;
  block1870: assert (this != null); goto $$block1870~e;
  $$block1870~e: stack0i := $Heap[this, Friend.x]; goto $$block1870~d;
  $$block1870~d: assert (this != null); goto $$block1870~c;
  $$block1870~c: stack1o := $Heap[this, Friend.th]; goto $$block1870~b;
  $$block1870~b: assert (stack1o != null); goto $$block1870~a;
  $$block1870~a: stack1i := $Heap[stack1o, Thing.y]; goto true1870to1972, false1870to1887;
  block1785: stack0b := throwException; goto true1785to1836, false1785to1802;
  true1785to1836: assume !stack0b; goto block1836;
  false1785to1802: assume stack0b; goto block1802;
  block1836: local0 := false; goto block2091;
  block1802: assume false; goto $$block1802~i;
  $$block1802~i: havoc stack50000o; goto $$block1802~h;
  $$block1802~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block1802~g;
  $$block1802~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block1802~f;
  $$block1802~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block1802~e;
  $$block1802~e: assert (stack50000o != null); goto $$block1802~d;
  $$block1802~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block1802~c;
  $$block1802~c: stack0o := stack50000o; goto $$block1802~b;
  $$block1802~b: assert (stack0o != null); goto $$block1802~a;
  $$block1802~a: assume false; return;
  true1870to1972: assume (stack0i == stack1i); goto block1972;
  false1870to1887: assume (stack0i != stack1i); goto block1887;
  block1972: assert (this != null); goto $$block1972~c;
  $$block1972~c: stack0o := $Heap[this, Friend.th]; goto $$block1972~b;
  $$block1972~b: assert (stack0o != null); goto $$block1972~a;
  $$block1972~a: stack0o := $Heap[stack0o, Thing.f]; goto true1972to2074, false1972to1989;
  block1887: stack0b := throwException; goto true1887to1938, false1887to1904;
  true1887to1938: assume !stack0b; goto block1938;
  false1887to1904: assume stack0b; goto block1904;
  block1938: local0 := false; goto block2091;
  block1904: assume false; goto $$block1904~i;
  $$block1904~i: havoc stack50000o; goto $$block1904~h;
  $$block1904~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block1904~g;
  $$block1904~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block1904~f;
  $$block1904~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block1904~e;
  $$block1904~e: assert (stack50000o != null); goto $$block1904~d;
  $$block1904~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block1904~c;
  $$block1904~c: stack0o := stack50000o; goto $$block1904~b;
  $$block1904~b: assert (stack0o != null); goto $$block1904~a;
  $$block1904~a: assume false; return;
  true1972to2074: assume (stack0o == this); goto block2074;
  false1972to1989: assume (stack0o != this); goto block1989;
  block2074: local0 := true; goto block2091;
  block1989: stack0b := throwException; goto true1989to2040, false1989to2006;
  block2091: SS$Display.Return.Local := local0; goto $$block2091~b;
  $$block2091~b: stack0b := local0; goto $$block2091~a;
  $$block2091~a: $result := stack0b; return;
  true1989to2040: assume !stack0b; goto block2040;
  false1989to2006: assume stack0b; goto block2006;
  block2040: local0 := false; goto block2091;
  block2006: assume false; goto $$block2006~i;
  $$block2006~i: havoc stack50000o; goto $$block2006~h;
  $$block2006~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block2006~g;
  $$block2006~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block2006~f;
  $$block2006~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block2006~e;
  $$block2006~e: assert (stack50000o != null); goto $$block2006~d;
  $$block2006~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block2006~c;
  $$block2006~c: stack0o := stack50000o; goto $$block2006~b;
  $$block2006~b: assert (stack0o != null); goto $$block2006~a;
  $$block2006~a: assume false; return;
  
}

axiom (Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException);
axiom (Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException);
axiom (System.Exception <: System.Exception);
axiom ($BaseClass(System.Exception) == System.Object);
axiom ((System.Exception <: $BaseClass(System.Exception)) && (AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception));
axiom (!$IsImmutable(System.Exception) && ($AsMutable(System.Exception) == System.Exception));
axiom (System.Runtime.Serialization.ISerializable <: System.Object);
axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable);
axiom (System.Exception <: System.Runtime.Serialization.ISerializable);
axiom (System.Runtime.InteropServices._Exception <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Exception);
axiom (System.Exception <: System.Runtime.InteropServices._Exception);
axiom ($BaseClass(Microsoft.Contracts.GuardException) == System.Exception);
axiom ((Microsoft.Contracts.GuardException <: $BaseClass(Microsoft.Contracts.GuardException)) && (AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException));
axiom (!$IsImmutable(Microsoft.Contracts.GuardException) && ($AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException));
axiom ($BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException);
axiom ((Microsoft.Contracts.ObjectInvariantException <: $BaseClass(Microsoft.Contracts.ObjectInvariantException)) && (AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException));
axiom (!$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && ($AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException));
procedure Microsoft.Contracts.ObjectInvariantException..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Microsoft.Contracts.ObjectInvariantException <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure Friend..ctor$Thing$notnull(this : ref, thing$in : ref where $IsNotNull(thing$in, Thing));
  requires ($Heap[thing$in, $ownerFrame] == $PeerGroupPlaceholder);
  free requires ($Heap[thing$in, $allocated] == true);
  requires ($Heap[thing$in, Thing.f] == null);
  requires (((($Heap[thing$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[thing$in, $ownerRef], $inv] <: $Heap[thing$in, $ownerFrame])) || ($Heap[$Heap[thing$in, $ownerRef], $localinv] == $BaseClass($Heap[thing$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[thing$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[thing$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Friend)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[thing$in, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[thing$in, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Friend <: DeclType($f)))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[thing$in, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[thing$in, $ownerFrame]))))) && old((($o != thing$in) || ($f != Thing.f)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation Friend..ctor$Thing$notnull(this : ref, thing$in : ref) {
  var thing : ref where $IsNotNull(thing, Thing);
  var stack0o : ref;
  var stack1o : ref;
  var stack0i : int;
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local3 : ref where $Is(local3, System.Exception);
  var stack0b : bool;
  var temp2 : ref;
  entry: assume $IsNotNull(this, Friend); goto $$entry~g;
  $$entry~g: assume ($Heap[this, $allocated] == true); goto $$entry~f;
  $$entry~f: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~e;
  $$entry~e: thing := thing$in; goto $$entry~d;
  $$entry~d: assume ($Heap[this, Friend.x] == 0); goto $$entry~c;
  $$entry~c: assume ($Heap[this, Friend.th] == null); goto block3332;
  block3332: goto block3485;
  block3485: assert (this != null); goto $$block3485~c;
  $$block3485~c: call System.Object..ctor(this); goto $$block3485~b;
  $$block3485~b: $Heap := $Heap[this, $NonNullFieldsAreInitialized := true]; goto $$block3485~a;
  $$block3485~a: assume IsHeap($Heap); goto block3553;
  block3553: stack0o := thing; goto $$block3553~y;
  $$block3553~y: stack1o := this; goto $$block3553~x;
  $$block3553~x: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block3553~w;
  $$block3553~w: assert !$IsImmutable($typeof(stack0o)); goto $$block3553~v;
  $$block3553~v: assert !$IsImmutable($typeof(stack1o)); goto $$block3553~u;
  $$block3553~u: assert ((($Heap[stack1o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack1o, $ownerRef], $inv] <: $Heap[stack1o, $ownerFrame])) || ($Heap[$Heap[stack1o, $ownerRef], $localinv] == $BaseClass($Heap[stack1o, $ownerFrame]))); goto $$block3553~t;
  $$block3553~t: call $SetOwner(stack0o, $Heap[stack1o, $ownerRef], $Heap[stack1o, $ownerFrame]); goto $$block3553~s;
  $$block3553~s: assert (this != null); goto $$block3553~r;
  $$block3553~r: assert (!($Heap[this, $inv] <: Friend) || ($Heap[this, $localinv] == System.Object)); goto $$block3553~q;
  $$block3553~q: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Thing)) && ($Heap[$o, Thing.f] == this)) ==> (!($Heap[$o, $inv] <: Thing) || ($Heap[$o, $localinv] == System.Object)))); goto $$block3553~p;
  $$block3553~p: $Heap := $Heap[this, Friend.th := thing]; goto $$block3553~o;
  $$block3553~o: assume IsHeap($Heap); goto $$block3553~n;
  $$block3553~n: assert (thing != null); goto $$block3553~m;
  $$block3553~m: stack0i := $Heap[thing, Thing.y]; goto $$block3553~l;
  $$block3553~l: assert (this != null); goto $$block3553~k;
  $$block3553~k: assert (!($Heap[this, $inv] <: Friend) || ($Heap[this, $localinv] == System.Object)); goto $$block3553~j;
  $$block3553~j: $Heap := $Heap[this, Friend.x := stack0i]; goto $$block3553~i;
  $$block3553~i: assume IsHeap($Heap); goto $$block3553~h;
  $$block3553~h: temp0 := thing; goto $$block3553~g;
  $$block3553~g: assert (temp0 != null); goto $$block3553~f;
  $$block3553~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Thing)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block3553~e;
  $$block3553~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block3553~d;
  $$block3553~d: havoc temp1; goto $$block3553~c;
  $$block3553~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block3553~b;
  $$block3553~b: assume IsHeap($Heap); goto $$block3553~a;
  $$block3553~a: local3 := null; goto block3570;
  block3570: assert (thing != null); goto $$block3570~f;
  $$block3570~f: assert (!($Heap[thing, $inv] <: Thing) || ($Heap[thing, $localinv] == System.Object)); goto $$block3570~e;
  $$block3570~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Friend)) && ($Heap[$o, Friend.th] == thing)) ==> (!($Heap[$o, $inv] <: Friend) || ($Heap[$o, $localinv] == System.Object)))); goto $$block3570~d;
  $$block3570~d: assert (((((this == null) || (($Heap[thing, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[thing, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[thing, $ownerRef], $inv] <: $Heap[thing, $ownerFrame]) || ($Heap[$Heap[thing, $ownerRef], $localinv] == $BaseClass($Heap[thing, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[thing, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[thing, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block3570~c;
  $$block3570~c: $Heap := $Heap[thing, Thing.f := this]; goto $$block3570~b;
  $$block3570~b: call $UpdateOwnersForPeer(thing, this); goto $$block3570~a;
  $$block3570~a: assume IsHeap($Heap); goto block3655;
  block3655: stack0o := null; goto true3655to3723, false3655to3672;
  true3655to3723: assume (local3 == stack0o); goto block3723;
  false3655to3672: assume (local3 != stack0o); goto block3672;
  block3723: assert (temp0 != null); goto $$block3723~f;
  $$block3723~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block3723~e;
  $$block3723~e: assert (($Heap[temp0, Thing.f] == null) || ($Heap[$Heap[temp0, Thing.f], Friend.th] == temp0)); goto $$block3723~d;
  $$block3723~d: assert (0 <= $Heap[temp0, Thing.y]); goto $$block3723~c;
  $$block3723~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block3723~b;
  $$block3723~b: $Heap := $Heap[temp0, $inv := Thing]; goto $$block3723~a;
  $$block3723~a: assume IsHeap($Heap); goto block3706;
  block3672: goto true3672to3723, false3672to3689;
  true3672to3723: assume ($As(local3, Microsoft.Contracts.ICheckedException) != null); goto block3723;
  false3672to3689: assume ($As(local3, Microsoft.Contracts.ICheckedException) == null); goto block3689;
  block3689: goto block3706;
  block3706: goto block3621;
  block3621: temp2 := this; goto $$block3621~h;
  $$block3621~h: assert (temp2 != null); goto $$block3621~g;
  $$block3621~g: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block3621~f;
  $$block3621~f: assert ($Heap[temp2, Friend.th] != null); goto $$block3621~e;
  $$block3621~e: assert ($Heap[temp2, Friend.x] == $Heap[$Heap[temp2, Friend.th], Thing.y]); goto $$block3621~d;
  $$block3621~d: assert ($Heap[$Heap[temp2, Friend.th], Thing.f] == temp2); goto $$block3621~c;
  $$block3621~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Friend)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block3621~b;
  $$block3621~b: $Heap := $Heap[temp2, $inv := Friend]; goto $$block3621~a;
  $$block3621~a: assume IsHeap($Heap); return;
  
}

procedure System.Object..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(System.Object <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

axiom (Microsoft.Contracts.ICheckedException <: System.Object);
axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException);
procedure Friend..ctor$Thing$notnull$System.Boolean(this : ref, thing$in : ref where $IsNotNull(thing$in, Thing), disambiguator$in : bool where true);
  free requires ($Heap[thing$in, $allocated] == true);
  free requires true;
  requires ($Heap[thing$in, Thing.f] == null);
  requires (((($Heap[thing$in, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[thing$in, $ownerRef], $inv] <: $Heap[thing$in, $ownerFrame])) || ($Heap[$Heap[thing$in, $ownerRef], $localinv] == $BaseClass($Heap[thing$in, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[thing$in, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[thing$in, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Friend)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] == true)) && ((old($Heap)[$o, $ownerRef] != old($Heap)[this, $ownerRef]) || (old($Heap)[$o, $ownerFrame] != old($Heap)[this, $ownerFrame]))) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} ((((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Friend <: DeclType($f)))) && !((($f == $ownerRef) || ($f == $ownerFrame)) && old((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame]))))) && old((($o != thing$in) || ($f != Thing.f)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation Friend..ctor$Thing$notnull$System.Boolean(this : ref, thing$in : ref, disambiguator$in : bool) {
  var thing : ref where $IsNotNull(thing, Thing);
  var disambiguator : bool where true;
  var stack0o : ref;
  var stack1o : ref;
  var stack0i : int;
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local3 : ref where $Is(local3, System.Exception);
  var stack0b : bool;
  var temp2 : ref;
  entry: assume $IsNotNull(this, Friend); goto $$entry~m;
  $$entry~m: assume ($Heap[this, $allocated] == true); goto $$entry~l;
  $$entry~l: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~k;
  $$entry~k: thing := thing$in; goto $$entry~j;
  $$entry~j: disambiguator := disambiguator$in; goto $$entry~i;
  $$entry~i: assume ($Heap[this, Friend.x] == 0); goto $$entry~h;
  $$entry~h: assume ($Heap[this, Friend.th] == null); goto block4930;
  block4930: goto block5083;
  block5083: assert (this != null); goto $$block5083~c;
  $$block5083~c: call System.Object..ctor(this); goto $$block5083~b;
  $$block5083~b: $Heap := $Heap[this, $NonNullFieldsAreInitialized := true]; goto $$block5083~a;
  $$block5083~a: assume IsHeap($Heap); goto block5151;
  block5151: stack0o := this; goto $$block5151~y;
  $$block5151~y: stack1o := thing; goto $$block5151~x;
  $$block5151~x: assert ($Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder); goto $$block5151~w;
  $$block5151~w: assert !$IsImmutable($typeof(stack0o)); goto $$block5151~v;
  $$block5151~v: assert !$IsImmutable($typeof(stack1o)); goto $$block5151~u;
  $$block5151~u: assert ((($Heap[stack1o, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[stack1o, $ownerRef], $inv] <: $Heap[stack1o, $ownerFrame])) || ($Heap[$Heap[stack1o, $ownerRef], $localinv] == $BaseClass($Heap[stack1o, $ownerFrame]))); goto $$block5151~t;
  $$block5151~t: call $SetOwner(stack0o, $Heap[stack1o, $ownerRef], $Heap[stack1o, $ownerFrame]); goto $$block5151~s;
  $$block5151~s: assert (this != null); goto $$block5151~r;
  $$block5151~r: assert (!($Heap[this, $inv] <: Friend) || ($Heap[this, $localinv] == System.Object)); goto $$block5151~q;
  $$block5151~q: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Thing)) && ($Heap[$o, Thing.f] == this)) ==> (!($Heap[$o, $inv] <: Thing) || ($Heap[$o, $localinv] == System.Object)))); goto $$block5151~p;
  $$block5151~p: $Heap := $Heap[this, Friend.th := thing]; goto $$block5151~o;
  $$block5151~o: assume IsHeap($Heap); goto $$block5151~n;
  $$block5151~n: assert (thing != null); goto $$block5151~m;
  $$block5151~m: stack0i := $Heap[thing, Thing.y]; goto $$block5151~l;
  $$block5151~l: assert (this != null); goto $$block5151~k;
  $$block5151~k: assert (!($Heap[this, $inv] <: Friend) || ($Heap[this, $localinv] == System.Object)); goto $$block5151~j;
  $$block5151~j: $Heap := $Heap[this, Friend.x := stack0i]; goto $$block5151~i;
  $$block5151~i: assume IsHeap($Heap); goto $$block5151~h;
  $$block5151~h: temp0 := thing; goto $$block5151~g;
  $$block5151~g: assert (temp0 != null); goto $$block5151~f;
  $$block5151~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Thing)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block5151~e;
  $$block5151~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block5151~d;
  $$block5151~d: havoc temp1; goto $$block5151~c;
  $$block5151~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block5151~b;
  $$block5151~b: assume IsHeap($Heap); goto $$block5151~a;
  $$block5151~a: local3 := null; goto block5168;
  block5168: assert (thing != null); goto $$block5168~f;
  $$block5168~f: assert (!($Heap[thing, $inv] <: Thing) || ($Heap[thing, $localinv] == System.Object)); goto $$block5168~e;
  $$block5168~e: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Friend)) && ($Heap[$o, Friend.th] == thing)) ==> (!($Heap[$o, $inv] <: Friend) || ($Heap[$o, $localinv] == System.Object)))); goto $$block5168~d;
  $$block5168~d: assert (((((this == null) || (($Heap[thing, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[thing, $ownerFrame] == $PeerGroupPlaceholder) && (!($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))))) || ((!($Heap[$Heap[thing, $ownerRef], $inv] <: $Heap[thing, $ownerFrame]) || ($Heap[$Heap[thing, $ownerRef], $localinv] == $BaseClass($Heap[thing, $ownerFrame]))) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder))) || (($Heap[thing, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[thing, $ownerFrame] == $Heap[this, $ownerFrame]))); goto $$block5168~c;
  $$block5168~c: $Heap := $Heap[thing, Thing.f := this]; goto $$block5168~b;
  $$block5168~b: call $UpdateOwnersForPeer(thing, this); goto $$block5168~a;
  $$block5168~a: assume IsHeap($Heap); goto block5253;
  block5253: stack0o := null; goto true5253to5321, false5253to5270;
  true5253to5321: assume (local3 == stack0o); goto block5321;
  false5253to5270: assume (local3 != stack0o); goto block5270;
  block5321: assert (temp0 != null); goto $$block5321~f;
  $$block5321~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block5321~e;
  $$block5321~e: assert (($Heap[temp0, Thing.f] == null) || ($Heap[$Heap[temp0, Thing.f], Friend.th] == temp0)); goto $$block5321~d;
  $$block5321~d: assert (0 <= $Heap[temp0, Thing.y]); goto $$block5321~c;
  $$block5321~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block5321~b;
  $$block5321~b: $Heap := $Heap[temp0, $inv := Thing]; goto $$block5321~a;
  $$block5321~a: assume IsHeap($Heap); goto block5304;
  block5270: goto true5270to5321, false5270to5287;
  true5270to5321: assume ($As(local3, Microsoft.Contracts.ICheckedException) != null); goto block5321;
  false5270to5287: assume ($As(local3, Microsoft.Contracts.ICheckedException) == null); goto block5287;
  block5287: goto block5304;
  block5304: goto block5219;
  block5219: temp2 := this; goto $$block5219~h;
  $$block5219~h: assert (temp2 != null); goto $$block5219~g;
  $$block5219~g: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block5219~f;
  $$block5219~f: assert ($Heap[temp2, Friend.th] != null); goto $$block5219~e;
  $$block5219~e: assert ($Heap[temp2, Friend.x] == $Heap[$Heap[temp2, Friend.th], Thing.y]); goto $$block5219~d;
  $$block5219~d: assert ($Heap[$Heap[temp2, Friend.th], Thing.f] == temp2); goto $$block5219~c;
  $$block5219~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Friend)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block5219~b;
  $$block5219~b: $Heap := $Heap[temp2, $inv := Friend]; goto $$block5219~a;
  $$block5219~a: assume IsHeap($Heap); return;
  
}

procedure Friend..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Friend..cctor() {
  entry: goto block6443;
  block6443: goto block6494;
  block6494: return;
  
}

procedure Thing.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0o : ref;
  var stack1o : ref;
  var stack0b : bool;
  var stack0i : int;
  var stack1i : int;
  var local0 : bool where true;
  var stack50000o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, Thing); goto $$entry~o;
  $$entry~o: assume ($Heap[this, $allocated] == true); goto $$entry~n;
  $$entry~n: throwException := throwException$in; goto block6936;
  block6936: goto block6953;
  block6953: assert (this != null); goto $$block6953~b;
  $$block6953~b: stack0o := $Heap[this, Thing.f]; goto $$block6953~a;
  $$block6953~a: stack1o := null; goto true6953to7072, false6953to6970;
  true6953to7072: assume (stack0o == stack1o); goto block7072;
  false6953to6970: assume (stack0o != stack1o); goto block6970;
  block7072: stack0i := 0; goto $$block7072~b;
  $$block7072~b: assert (this != null); goto $$block7072~a;
  $$block7072~a: stack1i := $Heap[this, Thing.y]; goto true7072to7174, false7072to7089;
  block6970: assert (this != null); goto $$block6970~c;
  $$block6970~c: stack0o := $Heap[this, Thing.f]; goto $$block6970~b;
  $$block6970~b: assert (stack0o != null); goto $$block6970~a;
  $$block6970~a: stack0o := $Heap[stack0o, Friend.th]; goto true6970to7072, false6970to6987;
  true6970to7072: assume (stack0o == this); goto block7072;
  false6970to6987: assume (stack0o != this); goto block6987;
  block6987: stack0b := throwException; goto true6987to7038, false6987to7004;
  true7072to7174: assume (stack0i <= stack1i); goto block7174;
  false7072to7089: assume (stack0i > stack1i); goto block7089;
  block7174: local0 := true; goto block7191;
  block7089: stack0b := throwException; goto true7089to7140, false7089to7106;
  true6987to7038: assume !stack0b; goto block7038;
  false6987to7004: assume stack0b; goto block7004;
  block7038: local0 := false; goto block7191;
  block7004: assume false; goto $$block7004~i;
  $$block7004~i: havoc stack50000o; goto $$block7004~h;
  $$block7004~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block7004~g;
  $$block7004~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block7004~f;
  $$block7004~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block7004~e;
  $$block7004~e: assert (stack50000o != null); goto $$block7004~d;
  $$block7004~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block7004~c;
  $$block7004~c: stack0o := stack50000o; goto $$block7004~b;
  $$block7004~b: assert (stack0o != null); goto $$block7004~a;
  $$block7004~a: assume false; return;
  true7089to7140: assume !stack0b; goto block7140;
  false7089to7106: assume stack0b; goto block7106;
  block7140: local0 := false; goto block7191;
  block7106: assume false; goto $$block7106~i;
  $$block7106~i: havoc stack50000o; goto $$block7106~h;
  $$block7106~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block7106~g;
  $$block7106~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block7106~f;
  $$block7106~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block7106~e;
  $$block7106~e: assert (stack50000o != null); goto $$block7106~d;
  $$block7106~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block7106~c;
  $$block7106~c: stack0o := stack50000o; goto $$block7106~b;
  $$block7106~b: assert (stack0o != null); goto $$block7106~a;
  $$block7106~a: assume false; return;
  block7191: SS$Display.Return.Local := local0; goto $$block7191~b;
  $$block7191~b: stack0b := local0; goto $$block7191~a;
  $$block7191~a: $result := stack0b; return;
  
}

procedure Thing..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Thing)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Thing <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation Thing..ctor(this : ref) {
  var temp0 : ref;
  entry: assume $IsNotNull(this, Thing); goto $$entry~s;
  $$entry~s: assume ($Heap[this, $allocated] == true); goto $$entry~r;
  $$entry~r: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~q;
  $$entry~q: assume ($Heap[this, Thing.f] == null); goto $$entry~p;
  $$entry~p: assume ($Heap[this, Thing.y] == 0); goto block7956;
  block7956: goto block7973;
  block7973: assert (this != null); goto $$block7973~a;
  $$block7973~a: call System.Object..ctor(this); goto block8041;
  block8041: temp0 := this; goto $$block8041~g;
  $$block8041~g: assert (temp0 != null); goto $$block8041~f;
  $$block8041~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block8041~e;
  $$block8041~e: assert (($Heap[temp0, Thing.f] == null) || ($Heap[$Heap[temp0, Thing.f], Friend.th] == temp0)); goto $$block8041~d;
  $$block8041~d: assert (0 <= $Heap[temp0, Thing.y]); goto $$block8041~c;
  $$block8041~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block8041~b;
  $$block8041~b: $Heap := $Heap[temp0, $inv := Thing]; goto $$block8041~a;
  $$block8041~a: assume IsHeap($Heap); return;
  
}

axiom (System.Type <: System.Type);
axiom (System.Reflection.MemberInfo <: System.Reflection.MemberInfo);
axiom ($BaseClass(System.Reflection.MemberInfo) == System.Object);
axiom ((System.Reflection.MemberInfo <: $BaseClass(System.Reflection.MemberInfo)) && (AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo));
axiom ($IsImmutable(System.Reflection.MemberInfo) && ($AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo));
axiom (System.Reflection.ICustomAttributeProvider <: System.Object);
axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider);
axiom (System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider);
axiom (System.Runtime.InteropServices._MemberInfo <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo);
axiom (System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo);
axiom $IsMemberlessType(System.Reflection.MemberInfo);
axiom ($BaseClass(System.Type) == System.Reflection.MemberInfo);
axiom ((System.Type <: $BaseClass(System.Type)) && (AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type));
axiom ($IsImmutable(System.Type) && ($AsImmutable(System.Type) == System.Type));
axiom (System.Runtime.InteropServices._Type <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Type);
axiom (System.Type <: System.Runtime.InteropServices._Type);
axiom (System.Reflection.IReflect <: System.Object);
axiom $IsMemberlessType(System.Reflection.IReflect);
axiom (System.Type <: System.Reflection.IReflect);
axiom $IsMemberlessType(System.Type);
procedure Thing.P(this : ref);
  requires (($Heap[this, Thing.f] != null) && (TypeObject($typeof($Heap[this, Thing.f])) == TypeObject(Friend)));
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing.P(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var stack0o : ref;
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var local5 : int where InRange(local5, System.Int32);
  var stack0i : int;
  var local6 : ref where $Is(local6, Friend);
  var local7 : int where InRange(local7, System.Int32);
  var stack0b : bool;
  entry: assume $IsNotNull(this, Thing); goto $$entry~t;
  $$entry~t: assume ($Heap[this, $allocated] == true); goto block8925;
  block8925: goto block9146;
  block9146: temp0 := this; goto $$block9146~g;
  $$block9146~g: assert (temp0 != null); goto $$block9146~f;
  $$block9146~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Thing)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block9146~e;
  $$block9146~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block9146~d;
  $$block9146~d: havoc temp1; goto $$block9146~c;
  $$block9146~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block9146~b;
  $$block9146~b: assume IsHeap($Heap); goto $$block9146~a;
  $$block9146~a: local2 := null; goto block9163;
  block9163: assert (this != null); goto $$block9163~i;
  $$block9163~i: stack0o := $Heap[this, Thing.f]; goto $$block9163~h;
  $$block9163~h: temp2 := stack0o; goto $$block9163~g;
  $$block9163~g: assert (temp2 != null); goto $$block9163~f;
  $$block9163~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Friend)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block9163~e;
  $$block9163~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block9163~d;
  $$block9163~d: havoc temp3; goto $$block9163~c;
  $$block9163~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block9163~b;
  $$block9163~b: assume IsHeap($Heap); goto $$block9163~a;
  $$block9163~a: local4 := null; goto block9180;
  block9180: assert (this != null); goto $$block9180~t;
  $$block9180~t: local5 := $Heap[this, Thing.y]; goto $$block9180~s;
  $$block9180~s: stack0i := 1; goto $$block9180~r;
  $$block9180~r: stack0i := (local5 + stack0i); goto $$block9180~q;
  $$block9180~q: assert (this != null); goto $$block9180~p;
  $$block9180~p: assert (!($Heap[this, $inv] <: Thing) || ($Heap[this, $localinv] == System.Object)); goto $$block9180~o;
  $$block9180~o: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Friend)) && ($Heap[$o, Friend.th] == this)) ==> (!($Heap[$o, $inv] <: Friend) || ($Heap[$o, $localinv] == System.Object)))); goto $$block9180~n;
  $$block9180~n: $Heap := $Heap[this, Thing.y := stack0i]; goto $$block9180~m;
  $$block9180~m: assume IsHeap($Heap); goto $$block9180~l;
  $$block9180~l: stack0i := local5; goto $$block9180~k;
  $$block9180~k: assert (this != null); goto $$block9180~j;
  $$block9180~j: local6 := $Heap[this, Thing.f]; goto $$block9180~i;
  $$block9180~i: assert (local6 != null); goto $$block9180~h;
  $$block9180~h: local7 := $Heap[local6, Friend.x]; goto $$block9180~g;
  $$block9180~g: stack0i := 1; goto $$block9180~f;
  $$block9180~f: stack0i := (local7 + stack0i); goto $$block9180~e;
  $$block9180~e: assert (local6 != null); goto $$block9180~d;
  $$block9180~d: assert (!($Heap[local6, $inv] <: Friend) || ($Heap[local6, $localinv] == System.Object)); goto $$block9180~c;
  $$block9180~c: $Heap := $Heap[local6, Friend.x := stack0i]; goto $$block9180~b;
  $$block9180~b: assume IsHeap($Heap); goto $$block9180~a;
  $$block9180~a: stack0i := local7; goto block9316;
  block9316: stack0o := null; goto true9316to9384, false9316to9333;
  true9316to9384: assume (local4 == stack0o); goto block9384;
  false9316to9333: assume (local4 != stack0o); goto block9333;
  block9384: assert (temp2 != null); goto $$block9384~g;
  $$block9384~g: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block9384~f;
  $$block9384~f: assert ($Heap[temp2, Friend.th] != null); goto $$block9384~e;
  $$block9384~e: assert ($Heap[temp2, Friend.x] == $Heap[$Heap[temp2, Friend.th], Thing.y]); goto $$block9384~d;
  $$block9384~d: assert ($Heap[$Heap[temp2, Friend.th], Thing.f] == temp2); goto $$block9384~c;
  $$block9384~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Friend)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block9384~b;
  $$block9384~b: $Heap := $Heap[temp2, $inv := Friend]; goto $$block9384~a;
  $$block9384~a: assume IsHeap($Heap); goto block9367;
  block9333: goto true9333to9384, false9333to9350;
  true9333to9384: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block9384;
  false9333to9350: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block9350;
  block9350: goto block9367;
  block9367: goto block9231;
  block9231: goto block9486;
  block9486: stack0o := null; goto true9486to9554, false9486to9503;
  true9486to9554: assume (local2 == stack0o); goto block9554;
  false9486to9503: assume (local2 != stack0o); goto block9503;
  block9554: assert (temp0 != null); goto $$block9554~f;
  $$block9554~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block9554~e;
  $$block9554~e: assert (($Heap[temp0, Thing.f] == null) || ($Heap[$Heap[temp0, Thing.f], Friend.th] == temp0)); goto $$block9554~d;
  $$block9554~d: assert (0 <= $Heap[temp0, Thing.y]); goto $$block9554~c;
  $$block9554~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block9554~b;
  $$block9554~b: $Heap := $Heap[temp0, $inv := Thing]; goto $$block9554~a;
  $$block9554~a: assume IsHeap($Heap); goto block9537;
  block9503: goto true9503to9554, false9503to9520;
  true9503to9554: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block9554;
  false9503to9520: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block9520;
  block9520: goto block9537;
  block9537: goto block9282;
  block9282: return;
  
}

procedure Thing.Q(this : ref);
  requires ($Heap[this, Thing.f] != null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing.Q(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var stack0o : ref;
  var temp2 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp3 : exposeVersionType;
  var local4 : ref where $Is(local4, System.Exception);
  var local5 : int where InRange(local5, System.Int32);
  var stack0i : int;
  var local6 : ref where $Is(local6, Friend);
  var local7 : int where InRange(local7, System.Int32);
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, Thing); goto $$entry~u;
  $$entry~u: assume ($Heap[this, $allocated] == true); goto block11339;
  block11339: goto block11543;
  block11543: temp0 := this; goto $$block11543~g;
  $$block11543~g: assert (temp0 != null); goto $$block11543~f;
  $$block11543~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Thing)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block11543~e;
  $$block11543~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block11543~d;
  $$block11543~d: havoc temp1; goto $$block11543~c;
  $$block11543~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block11543~b;
  $$block11543~b: assume IsHeap($Heap); goto $$block11543~a;
  $$block11543~a: local2 := null; goto block11560;
  block11560: assert (this != null); goto $$block11560~l;
  $$block11560~l: stack0o := $Heap[this, Thing.f]; goto $$block11560~k;
  $$block11560~k: temp2 := stack0o; goto $$block11560~j;
  $$block11560~j: havoc stack1s; goto $$block11560~i;
  $$block11560~i: assume $IsTokenForType(stack1s, Friend); goto $$block11560~h;
  $$block11560~h: stack1o := TypeObject(Friend); goto $$block11560~g;
  $$block11560~g: assert (temp2 != null); goto $$block11560~f;
  $$block11560~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] <: Friend)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block11560~e;
  $$block11560~e: $Heap := $Heap[temp2, $localinv := System.Object]; goto $$block11560~d;
  $$block11560~d: havoc temp3; goto $$block11560~c;
  $$block11560~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block11560~b;
  $$block11560~b: assume IsHeap($Heap); goto $$block11560~a;
  $$block11560~a: local4 := null; goto block11577;
  block11577: assert (this != null); goto $$block11577~t;
  $$block11577~t: local5 := $Heap[this, Thing.y]; goto $$block11577~s;
  $$block11577~s: stack0i := 1; goto $$block11577~r;
  $$block11577~r: stack0i := (local5 + stack0i); goto $$block11577~q;
  $$block11577~q: assert (this != null); goto $$block11577~p;
  $$block11577~p: assert (!($Heap[this, $inv] <: Thing) || ($Heap[this, $localinv] == System.Object)); goto $$block11577~o;
  $$block11577~o: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Friend)) && ($Heap[$o, Friend.th] == this)) ==> (!($Heap[$o, $inv] <: Friend) || ($Heap[$o, $localinv] == System.Object)))); goto $$block11577~n;
  $$block11577~n: $Heap := $Heap[this, Thing.y := stack0i]; goto $$block11577~m;
  $$block11577~m: assume IsHeap($Heap); goto $$block11577~l;
  $$block11577~l: stack0i := local5; goto $$block11577~k;
  $$block11577~k: assert (this != null); goto $$block11577~j;
  $$block11577~j: local6 := $Heap[this, Thing.f]; goto $$block11577~i;
  $$block11577~i: assert (local6 != null); goto $$block11577~h;
  $$block11577~h: local7 := $Heap[local6, Friend.x]; goto $$block11577~g;
  $$block11577~g: stack0i := 1; goto $$block11577~f;
  $$block11577~f: stack0i := (local7 + stack0i); goto $$block11577~e;
  $$block11577~e: assert (local6 != null); goto $$block11577~d;
  $$block11577~d: assert (!($Heap[local6, $inv] <: Friend) || ($Heap[local6, $localinv] == System.Object)); goto $$block11577~c;
  $$block11577~c: $Heap := $Heap[local6, Friend.x := stack0i]; goto $$block11577~b;
  $$block11577~b: assume IsHeap($Heap); goto $$block11577~a;
  $$block11577~a: stack0i := local7; goto block11713;
  block11713: stack0o := null; goto true11713to11781, false11713to11730;
  true11713to11781: assume (local4 == stack0o); goto block11781;
  false11713to11730: assume (local4 != stack0o); goto block11730;
  block11781: havoc stack0s; goto $$block11781~j;
  $$block11781~j: assume $IsTokenForType(stack0s, Friend); goto $$block11781~i;
  $$block11781~i: stack0o := TypeObject(Friend); goto $$block11781~h;
  $$block11781~h: assert (temp2 != null); goto $$block11781~g;
  $$block11781~g: assert ($Heap[temp2, $localinv] == System.Object); goto $$block11781~f;
  $$block11781~f: assert ($Heap[temp2, Friend.th] != null); goto $$block11781~e;
  $$block11781~e: assert ($Heap[temp2, Friend.x] == $Heap[$Heap[temp2, Friend.th], Thing.y]); goto $$block11781~d;
  $$block11781~d: assert ($Heap[$Heap[temp2, Friend.th], Thing.f] == temp2); goto $$block11781~c;
  $$block11781~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Friend)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block11781~b;
  $$block11781~b: $Heap := $Heap[temp2, $localinv := $typeof(temp2)]; goto $$block11781~a;
  $$block11781~a: assume IsHeap($Heap); goto block11764;
  block11730: goto true11730to11781, false11730to11747;
  true11730to11781: assume ($As(local4, Microsoft.Contracts.ICheckedException) != null); goto block11781;
  false11730to11747: assume ($As(local4, Microsoft.Contracts.ICheckedException) == null); goto block11747;
  block11747: goto block11764;
  block11764: goto block11628;
  block11628: goto block11883;
  block11883: stack0o := null; goto true11883to11951, false11883to11900;
  true11883to11951: assume (local2 == stack0o); goto block11951;
  false11883to11900: assume (local2 != stack0o); goto block11900;
  block11951: assert (temp0 != null); goto $$block11951~f;
  $$block11951~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block11951~e;
  $$block11951~e: assert (($Heap[temp0, Thing.f] == null) || ($Heap[$Heap[temp0, Thing.f], Friend.th] == temp0)); goto $$block11951~d;
  $$block11951~d: assert (0 <= $Heap[temp0, Thing.y]); goto $$block11951~c;
  $$block11951~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block11951~b;
  $$block11951~b: $Heap := $Heap[temp0, $inv := Thing]; goto $$block11951~a;
  $$block11951~a: assume IsHeap($Heap); goto block11934;
  block11900: goto true11900to11951, false11900to11917;
  true11900to11951: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block11951;
  false11900to11917: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block11917;
  block11917: goto block11934;
  block11934: goto block11679;
  block11679: return;
  
}

procedure Thing.R(this : ref);
  requires ($Heap[this, Thing.f] != null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing.R(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : ref where $Is(local3, Friend);
  var local4 : int where InRange(local4, System.Int32);
  var stack0i : int;
  var temp2 : ref;
  var temp3 : exposeVersionType;
  var local6 : ref where $Is(local6, System.Exception);
  var local7 : int where InRange(local7, System.Int32);
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, Thing); goto $$entry~v;
  $$entry~v: assume ($Heap[this, $allocated] == true); goto block13838;
  block13838: goto block14042;
  block14042: assert (this != null); goto $$block14042~l;
  $$block14042~l: stack0o := $Heap[this, Thing.f]; goto $$block14042~k;
  $$block14042~k: temp0 := stack0o; goto $$block14042~j;
  $$block14042~j: havoc stack1s; goto $$block14042~i;
  $$block14042~i: assume $IsTokenForType(stack1s, Friend); goto $$block14042~h;
  $$block14042~h: stack1o := TypeObject(Friend); goto $$block14042~g;
  $$block14042~g: assert (temp0 != null); goto $$block14042~f;
  $$block14042~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: Friend)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block14042~e;
  $$block14042~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block14042~d;
  $$block14042~d: havoc temp1; goto $$block14042~c;
  $$block14042~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block14042~b;
  $$block14042~b: assume IsHeap($Heap); goto $$block14042~a;
  $$block14042~a: local2 := null; goto block14059;
  block14059: assert (this != null); goto $$block14059~r;
  $$block14059~r: local3 := $Heap[this, Thing.f]; goto $$block14059~q;
  $$block14059~q: assert (local3 != null); goto $$block14059~p;
  $$block14059~p: local4 := $Heap[local3, Friend.x]; goto $$block14059~o;
  $$block14059~o: stack0i := 1; goto $$block14059~n;
  $$block14059~n: stack0i := (local4 + stack0i); goto $$block14059~m;
  $$block14059~m: assert (local3 != null); goto $$block14059~l;
  $$block14059~l: assert (!($Heap[local3, $inv] <: Friend) || ($Heap[local3, $localinv] == System.Object)); goto $$block14059~k;
  $$block14059~k: $Heap := $Heap[local3, Friend.x := stack0i]; goto $$block14059~j;
  $$block14059~j: assume IsHeap($Heap); goto $$block14059~i;
  $$block14059~i: stack0i := local4; goto $$block14059~h;
  $$block14059~h: temp2 := this; goto $$block14059~g;
  $$block14059~g: assert (temp2 != null); goto $$block14059~f;
  $$block14059~f: assert ((((($Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp2, $ownerRef], $inv] <: $Heap[temp2, $ownerFrame])) || ($Heap[$Heap[temp2, $ownerRef], $localinv] == $BaseClass($Heap[temp2, $ownerFrame]))) && ($Heap[temp2, $inv] == Thing)) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block14059~e;
  $$block14059~e: $Heap := $Heap[temp2, $inv := System.Object]; goto $$block14059~d;
  $$block14059~d: havoc temp3; goto $$block14059~c;
  $$block14059~c: $Heap := $Heap[temp2, $exposeVersion := temp3]; goto $$block14059~b;
  $$block14059~b: assume IsHeap($Heap); goto $$block14059~a;
  $$block14059~a: local6 := null; goto block14076;
  block14076: assert (this != null); goto $$block14076~i;
  $$block14076~i: local7 := $Heap[this, Thing.y]; goto $$block14076~h;
  $$block14076~h: stack0i := 1; goto $$block14076~g;
  $$block14076~g: stack0i := (local7 + stack0i); goto $$block14076~f;
  $$block14076~f: assert (this != null); goto $$block14076~e;
  $$block14076~e: assert (!($Heap[this, $inv] <: Thing) || ($Heap[this, $localinv] == System.Object)); goto $$block14076~d;
  $$block14076~d: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Friend)) && ($Heap[$o, Friend.th] == this)) ==> (!($Heap[$o, $inv] <: Friend) || ($Heap[$o, $localinv] == System.Object)))); goto $$block14076~c;
  $$block14076~c: $Heap := $Heap[this, Thing.y := stack0i]; goto $$block14076~b;
  $$block14076~b: assume IsHeap($Heap); goto $$block14076~a;
  $$block14076~a: stack0i := local7; goto block14212;
  block14212: stack0o := null; goto true14212to14280, false14212to14229;
  true14212to14280: assume (local6 == stack0o); goto block14280;
  false14212to14229: assume (local6 != stack0o); goto block14229;
  block14280: assert (temp2 != null); goto $$block14280~f;
  $$block14280~f: assert (($Heap[temp2, $inv] == System.Object) && ($Heap[temp2, $localinv] == $typeof(temp2))); goto $$block14280~e;
  $$block14280~e: assert (($Heap[temp2, Thing.f] == null) || ($Heap[$Heap[temp2, Thing.f], Friend.th] == temp2)); goto $$block14280~d;
  $$block14280~d: assert (0 <= $Heap[temp2, Thing.y]); goto $$block14280~c;
  $$block14280~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp2)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block14280~b;
  $$block14280~b: $Heap := $Heap[temp2, $inv := Thing]; goto $$block14280~a;
  $$block14280~a: assume IsHeap($Heap); goto block14263;
  block14229: goto true14229to14280, false14229to14246;
  true14229to14280: assume ($As(local6, Microsoft.Contracts.ICheckedException) != null); goto block14280;
  false14229to14246: assume ($As(local6, Microsoft.Contracts.ICheckedException) == null); goto block14246;
  block14246: goto block14263;
  block14263: goto block14127;
  block14127: goto block14382;
  block14382: stack0o := null; goto true14382to14450, false14382to14399;
  true14382to14450: assume (local2 == stack0o); goto block14450;
  false14382to14399: assume (local2 != stack0o); goto block14399;
  block14450: havoc stack0s; goto $$block14450~j;
  $$block14450~j: assume $IsTokenForType(stack0s, Friend); goto $$block14450~i;
  $$block14450~i: stack0o := TypeObject(Friend); goto $$block14450~h;
  $$block14450~h: assert (temp0 != null); goto $$block14450~g;
  $$block14450~g: assert ($Heap[temp0, $localinv] == System.Object); goto $$block14450~f;
  $$block14450~f: assert ($Heap[temp0, Friend.th] != null); goto $$block14450~e;
  $$block14450~e: assert ($Heap[temp0, Friend.x] == $Heap[$Heap[temp0, Friend.th], Thing.y]); goto $$block14450~d;
  $$block14450~d: assert ($Heap[$Heap[temp0, Friend.th], Thing.f] == temp0); goto $$block14450~c;
  $$block14450~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Friend)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block14450~b;
  $$block14450~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block14450~a;
  $$block14450~a: assume IsHeap($Heap); goto block14433;
  block14399: goto true14399to14450, false14399to14416;
  true14399to14450: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block14450;
  false14399to14416: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block14416;
  block14416: goto block14433;
  block14433: goto block14178;
  block14178: return;
  
}

procedure Thing.S(this : ref);
  requires ($Heap[this, Thing.f] != null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing.S(this : ref) {
  var stack0o : ref;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : ref where $Is(local3, Friend);
  var local4 : int where InRange(local4, System.Int32);
  var stack0i : int;
  var stack0b : bool;
  var stack0s : struct;
  entry: assume $IsNotNull(this, Thing); goto $$entry~w;
  $$entry~w: assume ($Heap[this, $allocated] == true); goto block16099;
  block16099: goto block16303;
  block16303: assert (this != null); goto $$block16303~l;
  $$block16303~l: stack0o := $Heap[this, Thing.f]; goto $$block16303~k;
  $$block16303~k: temp0 := stack0o; goto $$block16303~j;
  $$block16303~j: havoc stack1s; goto $$block16303~i;
  $$block16303~i: assume $IsTokenForType(stack1s, Friend); goto $$block16303~h;
  $$block16303~h: stack1o := TypeObject(Friend); goto $$block16303~g;
  $$block16303~g: assert (temp0 != null); goto $$block16303~f;
  $$block16303~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: Friend)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block16303~e;
  $$block16303~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block16303~d;
  $$block16303~d: havoc temp1; goto $$block16303~c;
  $$block16303~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block16303~b;
  $$block16303~b: assume IsHeap($Heap); goto $$block16303~a;
  $$block16303~a: local2 := null; goto block16320;
  block16320: assert (this != null); goto $$block16320~j;
  $$block16320~j: local3 := $Heap[this, Thing.f]; goto $$block16320~i;
  $$block16320~i: assert (local3 != null); goto $$block16320~h;
  $$block16320~h: local4 := $Heap[local3, Friend.x]; goto $$block16320~g;
  $$block16320~g: stack0i := 1; goto $$block16320~f;
  $$block16320~f: stack0i := (local4 + stack0i); goto $$block16320~e;
  $$block16320~e: assert (local3 != null); goto $$block16320~d;
  $$block16320~d: assert (!($Heap[local3, $inv] <: Friend) || ($Heap[local3, $localinv] == System.Object)); goto $$block16320~c;
  $$block16320~c: $Heap := $Heap[local3, Friend.x := stack0i]; goto $$block16320~b;
  $$block16320~b: assume IsHeap($Heap); goto $$block16320~a;
  $$block16320~a: stack0i := local4; goto block16405;
  block16405: stack0o := null; goto true16405to16473, false16405to16422;
  true16405to16473: assume (local2 == stack0o); goto block16473;
  false16405to16422: assume (local2 != stack0o); goto block16422;
  block16473: havoc stack0s; goto $$block16473~j;
  $$block16473~j: assume $IsTokenForType(stack0s, Friend); goto $$block16473~i;
  $$block16473~i: stack0o := TypeObject(Friend); goto $$block16473~h;
  $$block16473~h: assert (temp0 != null); goto $$block16473~g;
  $$block16473~g: assert ($Heap[temp0, $localinv] == System.Object); goto $$block16473~f;
  $$block16473~f: assert ($Heap[temp0, Friend.th] != null); goto $$block16473~e;
  $$block16473~e: assert ($Heap[temp0, Friend.x] == $Heap[$Heap[temp0, Friend.th], Thing.y]); goto $$block16473~d;
  $$block16473~d: assert ($Heap[$Heap[temp0, Friend.th], Thing.f] == temp0); goto $$block16473~c;
  $$block16473~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Friend)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block16473~b;
  $$block16473~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block16473~a;
  $$block16473~a: assume IsHeap($Heap); goto block16456;
  block16422: goto true16422to16473, false16422to16439;
  true16422to16473: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block16473;
  false16422to16439: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block16439;
  block16439: goto block16456;
  block16456: goto block16371;
  block16371: return;
  
}

procedure Thing.T(this : ref);
  requires ($Heap[this, Thing.f] != null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing.T(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Thing); goto $$entry~x;
  $$entry~x: assume ($Heap[this, $allocated] == true); goto block17663;
  block17663: goto block17867;
  block17867: temp0 := this; goto $$block17867~g;
  $$block17867~g: assert (temp0 != null); goto $$block17867~f;
  $$block17867~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Thing)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block17867~e;
  $$block17867~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block17867~d;
  $$block17867~d: havoc temp1; goto $$block17867~c;
  $$block17867~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block17867~b;
  $$block17867~b: assume IsHeap($Heap); goto $$block17867~a;
  $$block17867~a: local2 := null; goto block17884;
  block17884: assert (this != null); goto $$block17884~i;
  $$block17884~i: local3 := $Heap[this, Thing.y]; goto $$block17884~h;
  $$block17884~h: stack0i := 1; goto $$block17884~g;
  $$block17884~g: stack0i := (local3 + stack0i); goto $$block17884~f;
  $$block17884~f: assert (this != null); goto $$block17884~e;
  $$block17884~e: assert (!($Heap[this, $inv] <: Thing) || ($Heap[this, $localinv] == System.Object)); goto $$block17884~d;
  $$block17884~d: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Friend)) && ($Heap[$o, Friend.th] == this)) ==> (!($Heap[$o, $inv] <: Friend) || ($Heap[$o, $localinv] == System.Object)))); goto $$block17884~c;
  $$block17884~c: $Heap := $Heap[this, Thing.y := stack0i]; goto $$block17884~b;
  $$block17884~b: assume IsHeap($Heap); goto $$block17884~a;
  $$block17884~a: stack0i := local3; goto block17969;
  block17969: stack0o := null; goto true17969to18037, false17969to17986;
  true17969to18037: assume (local2 == stack0o); goto block18037;
  false17969to17986: assume (local2 != stack0o); goto block17986;
  block18037: assert (temp0 != null); goto $$block18037~f;
  $$block18037~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block18037~e;
  $$block18037~e: assert (($Heap[temp0, Thing.f] == null) || ($Heap[$Heap[temp0, Thing.f], Friend.th] == temp0)); goto $$block18037~d;
  $$block18037~d: assert (0 <= $Heap[temp0, Thing.y]); goto $$block18037~c;
  $$block18037~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block18037~b;
  $$block18037~b: $Heap := $Heap[temp0, $inv := Thing]; goto $$block18037~a;
  $$block18037~a: assume IsHeap($Heap); goto block18020;
  block17986: goto true17986to18037, false17986to18003;
  true17986to18037: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block18037;
  false17986to18003: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block18003;
  block18003: goto block18020;
  block18020: goto block17935;
  block17935: return;
  
}

procedure Thing.U(this : ref);
  requires ($Heap[this, Thing.f] == null);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing.U(this : ref) {
  var temp0 : ref;
  var temp1 : exposeVersionType;
  var local2 : ref where $Is(local2, System.Exception);
  var local3 : int where InRange(local3, System.Int32);
  var stack0i : int;
  var stack0o : ref;
  var stack0b : bool;
  entry: assume $IsNotNull(this, Thing); goto $$entry~y;
  $$entry~y: assume ($Heap[this, $allocated] == true); goto block19091;
  block19091: goto block19295;
  block19295: temp0 := this; goto $$block19295~g;
  $$block19295~g: assert (temp0 != null); goto $$block19295~f;
  $$block19295~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] == Thing)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block19295~e;
  $$block19295~e: $Heap := $Heap[temp0, $inv := System.Object]; goto $$block19295~d;
  $$block19295~d: havoc temp1; goto $$block19295~c;
  $$block19295~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block19295~b;
  $$block19295~b: assume IsHeap($Heap); goto $$block19295~a;
  $$block19295~a: local2 := null; goto block19312;
  block19312: assert (this != null); goto $$block19312~i;
  $$block19312~i: local3 := $Heap[this, Thing.y]; goto $$block19312~h;
  $$block19312~h: stack0i := 1; goto $$block19312~g;
  $$block19312~g: stack0i := (local3 + stack0i); goto $$block19312~f;
  $$block19312~f: assert (this != null); goto $$block19312~e;
  $$block19312~e: assert (!($Heap[this, $inv] <: Thing) || ($Heap[this, $localinv] == System.Object)); goto $$block19312~d;
  $$block19312~d: assert (forall $o : ref :: ((((($o != null) && ($Heap[$o, $allocated] == true)) && ($typeof($o) <: Friend)) && ($Heap[$o, Friend.th] == this)) ==> (!($Heap[$o, $inv] <: Friend) || ($Heap[$o, $localinv] == System.Object)))); goto $$block19312~c;
  $$block19312~c: $Heap := $Heap[this, Thing.y := stack0i]; goto $$block19312~b;
  $$block19312~b: assume IsHeap($Heap); goto $$block19312~a;
  $$block19312~a: stack0i := local3; goto block19397;
  block19397: stack0o := null; goto true19397to19465, false19397to19414;
  true19397to19465: assume (local2 == stack0o); goto block19465;
  false19397to19414: assume (local2 != stack0o); goto block19414;
  block19465: assert (temp0 != null); goto $$block19465~f;
  $$block19465~f: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block19465~e;
  $$block19465~e: assert (($Heap[temp0, Thing.f] == null) || ($Heap[$Heap[temp0, Thing.f], Friend.th] == temp0)); goto $$block19465~d;
  $$block19465~d: assert (0 <= $Heap[temp0, Thing.y]); goto $$block19465~c;
  $$block19465~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == Thing)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block19465~b;
  $$block19465~b: $Heap := $Heap[temp0, $inv := Thing]; goto $$block19465~a;
  $$block19465~a: assume IsHeap($Heap); goto block19448;
  block19414: goto true19414to19465, false19414to19431;
  true19414to19465: assume ($As(local2, Microsoft.Contracts.ICheckedException) != null); goto block19465;
  false19414to19431: assume ($As(local2, Microsoft.Contracts.ICheckedException) == null); goto block19431;
  block19431: goto block19448;
  block19448: goto block19363;
  block19363: return;
  
}

procedure Thing..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation Thing..cctor() {
  entry: goto block20179;
  block20179: goto block20230;
  block20230: return;
  
}

